\begin{tabbing}
$\forall$\=${\it Pgm}$, ${\it Sem}$:Type, ${\it equiv}$:(${\it Sem}$$\rightarrow$${\it Sem}$$\rightarrow$Prop), $X$:(${\it Sem}$$\rightarrow$Prop), $S$:(${\it Pgm}$$\rightarrow$${\it Sem}$), ${\it pr}$:${\it Pgm}$,\+
\\[0ex]${\it kpr}$:(${\it Sem}$$\rightarrow$${\it Pgm}$).
\-\\[0ex]${\it pr}$ implements ${\it kpr}$ $\Rightarrow$ ${\it kpr}$ $\vDash$ $X$ $\Rightarrow$ ${\it pr}$ $\vDash$ $X$
\end{tabbing}